$\forall$$A$:Type, $B_{1}$,$B_{2}$:($A$$\rightarrow$Type). \\[0ex]($\forall$$a$:$A$. subtype\_rel($B_{1}$($a$); $B_{2}$($a$))) $\Rightarrow$ subtype\_rel(fpf($A$; $a$.$B_{1}$($a$)); fpf($A$; $a$.$B_{2}$($a$)))